#ifndef _STORM_H_
#define _STORM_H_

#include "havoc.h"

int storm_nondet();
int storm_getThreadID();

void __storm_assert_dummy(void);
#define STORM_ASSERT(ASSRT) { \
  if (!(ASSRT)) { \
    __storm_assert_dummy(); \
  } \
}

void __storm_atomic_begin_dummy(void);
void __storm_atomic_end_dummy(void);
#define STORM_ATOMIC(BLOCK) { \
  __storm_atomic_begin_dummy(); \
  BLOCK; \
  __storm_atomic_end_dummy(); \
}

void __storm_init_begin_dummy(void);
void __storm_init_end_dummy(void);
#define STORM_INIT(BLOCK) { \
  __storm_init_begin_dummy(); \
  BLOCK; \
  __storm_init_end_dummy(); \
}

void __storm_end_dummy(void);
#define STORM_END { \
  __storm_end_dummy(); \
}

void __storm_switch_dummy(void);
#define SWITCH { \
  __storm_switch_dummy(); \
}


int k;
int errorReached;
int raiseException;

#define __preserve_globals __loop_assert(k == __old(k)) \
                           __loop_assert(errorReached == __old(errorReached)) \
                           __loop_assert(raiseException == __old(raiseException))

#endif

